﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace Epsilon
{
    public abstract class SecLabel
    {
        public override bool Equals(object obj)
        {
            return (obj is SecLabel) && this == ((SecLabel)obj);
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }

        public abstract Tuple<List<SecVar>, List<ISecPid>> Readers();

        public static bool operator ==(SecLabel left, SecLabel right)
        {
            if ((left is SecBase) && (right is SecBase))
                return (SecBase)left == (SecBase)right;

            if ((left is SecTuple) && (right is SecTuple))
                return (SecTuple)left == (SecTuple)right;

            if ((left is SecFun) && (right is SecFun))
                return (SecFun)left == (SecFun)right;

            return false;
        }

        public static bool operator !=(SecLabel left, SecLabel right)
        {
            return !(left == right);
        }
    }

    public class SecBase : SecLabel
    {
        public List<SecPolicy> Policies { get; private set; }
        public List<SecVar> Secvs { get; private set; }

        public SecBase(List<SecVar> v, List<SecPolicy> p)
        {
            Policies = p;
            Secvs = v;
        }

        public bool IsTop
        {
            get { return (Policies == null) && (Secvs == null); }
        }

        public override string ToString()
        {
            if (IsTop) 
                return "[]";

            string s = "";

            if (Secvs != null)
            {
                for (int i = 0; i < Secvs.Count; i++)
                {
                    if (i > 0)
                        s += " + ";
                    s += Secvs[i].ToString();
                }
            }
            if (Policies != null && Policies.Count > 0)
            {
                if (s != "")
                    s += " + ";
                s += "[";
                for (int i = 0; i < Policies.Count; i++)
                {
                    if (i > 0)
                        s += ", ";
                    s += Policies[i].ToString();
                }
                s += "]";
            }
            return s;
        }

        public override Tuple<List<SecVar>, List<ISecPid>> Readers()
        {
            List<ISecPid> pids = null;

            if (this.Policies != null)
            {
                for (int i = 0; i < this.Policies.Count; i++)
                {
                    if (pids == null)
                        pids = this.Policies[i].Readers;
                    else
                        pids = new List<ISecPid>(pids.Intersect(this.Policies[i].Readers));
                }
            }

            return new Tuple<List<SecVar>, List<ISecPid>>(this.Secvs, pids);
        }

        public static bool operator ==(SecBase left, SecBase right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.IsTop ^ right.IsTop)
                return false;

            if (left.IsTop && right.IsTop)
                return true;

            if ((left.Policies == null) ^ (right.Policies == null))
                return false;

            if (left.Policies != null && right.Policies != null)
            {
                foreach (SecPolicy sp in left.Policies)
                {
                    bool found = false;
                    foreach (SecPolicy ssp in right.Policies)
                    {
                        if (sp == ssp)
                        {
                            found = true;
                            break;
                        }
                    }
                    if (!found)
                        return false;
                }
                foreach (SecPolicy sp in right.Policies)
                {
                    bool found = false;
                    foreach (SecPolicy ssp in left.Policies)
                    {
                        if (sp == ssp)
                        {
                            found = true;
                            break;
                        }
                    }
                    if (!found)
                        return false;
                }
            }

            if ((left.Secvs == null) ^ (right.Secvs == null))
                return false;

            if (left.Secvs != null && right.Secvs != null)
            {
                foreach (SecVar se in left.Secvs)
                {
                    bool found = false;
                    foreach (SecVar sse in right.Secvs)
                    {
                        if (se == sse)
                        {
                            found = true;
                            break;
                        }
                    }
                    if (!found)
                        return false;
                }
                foreach (SecVar se in right.Secvs)
                {
                    bool found = false;
                    foreach (SecVar sse in left.Secvs)
                    {
                        if (se == sse)
                        {
                            found = true;
                            break;
                        }
                    }
                    if (!found)
                        return false;
                }
            }

            return true;
        }

        public static bool operator !=(SecBase left, SecBase right)
        {
            return !(left == right);
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }

        public override bool Equals(object obj)
        {
            return (obj is SecBase) && this == (SecBase)obj;
        }
    }

    public class SecTuple : SecLabel
    {
        public List<SecLabel> Labels { get; private set; }

        public SecTuple(List<SecLabel> ls)
        {
            Labels = ls;
        }

        public override string ToString()
        {
            string s = "{";

            for (int i = 0; i < Labels.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Labels[i].ToString();
            }

            return s + "}";
        }

        public override Tuple<List<SecVar>, List<ISecPid>> Readers()
        {
            List<SecVar> vars = null;
            List<ISecPid> pids = null;

            for (int i = 0; i < Labels.Count; i++)
            {
                Tuple<List<SecVar>, List<ISecPid>> r = Labels[i].Readers();

                if (pids == null)
                    pids = r.Item2;
                else if (r.Item2 != null)
                    pids = new List<ISecPid>(pids.Intersect(r.Item2));

                if (vars == null)
                    vars = r.Item1;
                else if (r.Item1 != null)
                    vars = new List<SecVar>(vars.Union(r.Item1));
            }

            return new Tuple<List<SecVar>, List<ISecPid>>(vars, pids);
        }

        public static bool operator ==(SecTuple left, SecTuple right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.Labels.Count != right.Labels.Count)
                return false;

            for (int i = 0; i < left.Labels.Count; i++)
            {
                if (left.Labels[i] != right.Labels[i])
                    return false;
            }
            return true;
        }

        public static bool operator !=(SecTuple left, SecTuple right)
        {
            return !(left == right);
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }

        public override bool Equals(object obj)
        {
            return (obj is SecTuple) && this == (SecTuple)obj;
        }
    }

    public class SecFun : SecLabel
    {
        public List<SecRLabel> Args { get; private set; }
        public SecLabel Ret { get; private set; }

        public SecFun(List<SecRLabel> a, SecLabel r)
        {
            Args = a;
            Ret = r;
        }

        public override Tuple<List<SecVar>, List<ISecPid>> Readers()
        {
            return Ret.Readers();
        }

        public override string ToString()
        {
            string s = "fun(";

            for (int i = 0; i < Args.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Args[i].ToString();
            }

            return s + ") -> " + Ret.ToString();
        }

        public static bool operator ==(SecFun left, SecFun right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.Args.Count != right.Args.Count)
                return false;

            bool alpha = false;
            for (int i = 0; i < left.Args.Count; i++)
            {
                if (left.Args[i] != right.Args[i])
                    alpha = true;
            }

            if (!alpha)
                return left.Ret == right.Ret;

            // else we alpha convert
            try
            {
                SecRTuple temp = new SecRTuple(left.Args);

                SecRLabel newAlpha = SecUtil.CreateNewAlpha(temp);
                SecRTuple oldLeft = new SecRTuple(left.Args);
                SecRTuple oldRight = new SecRTuple(right.Args);
                Dictionary<SecVar, SecVar> subLeft = SecUtil.Equate(oldLeft, newAlpha);
                Dictionary<SecVar, SecVar> subRight = SecUtil.Equate(oldRight, newAlpha);

                return (SecUtil.AlphaConvert(left, subLeft).Ret ==
                    SecUtil.AlphaConvert(right, subRight).Ret);
            }
            catch
            {
                return false;
            }
        }

        public static bool operator !=(SecFun left, SecFun right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is SecFun) && this == (SecFun)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public abstract class SecRLabel : SecLabel
    {
        public override bool Equals(object obj)
        {
            return (obj is SecRLabel) && this == ((SecRLabel)obj);
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }

        public static bool operator ==(SecRLabel left, SecRLabel right)
        {
            if ((left is SecVar) && (right is SecVar))
                return (SecVar)left == (SecVar)right;

            if ((left is SecRTuple) && (right is SecRTuple))
                return (SecRTuple)left == (SecRTuple)right;

            if ((left is SecRFun) && (right is SecRFun))
                return (SecRFun)left == (SecRFun)right;

            return false;
        }

        public static bool operator !=(SecRLabel left, SecRLabel right)
        {
            return !(left == right);
        }
    }

    public class SecVar : SecRLabel
    {
        public string SecV { get; private set; }

        public SecVar(string s)
        {
            SecV = s;
        }

        public override Tuple<List<SecVar>, List<ISecPid>> Readers()
        {
            return new Tuple<List<SecVar>, List<ISecPid>>(new List<SecVar>() { this }, null);
        }

        public override string ToString()
        {
            return SecV;
        }

        public static bool operator ==(SecVar left, SecVar right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            return left.SecV == right.SecV;
        }

        public static bool operator !=(SecVar left, SecVar right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is SecVar) && this == (SecVar)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public class SecRTuple : SecRLabel
    {
        public List<SecRLabel> Labels { get; private set; }

        public SecRTuple(List<SecRLabel> ls)
        {
            Labels = ls;
        }

        public override Tuple<List<SecVar>, List<ISecPid>> Readers()
        {
            List<SecVar> vars = null;
            List<ISecPid> pids = null;

            for (int i = 0; i < Labels.Count; i++)
            {
                Tuple<List<SecVar>, List<ISecPid>> r = Labels[i].Readers();

                if (pids == null)
                    pids = r.Item2;
                else
                    pids = new List<ISecPid>(pids.Intersect(r.Item2));

                if (vars == null)
                    vars = r.Item1;
                else
                    vars = new List<SecVar>(vars.Union(r.Item1));
            }

            return new Tuple<List<SecVar>, List<ISecPid>>(vars, pids);
        }

        public override string ToString()
        {
            string s = "{";

            for (int i = 0; i < Labels.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Labels[i].ToString();
            }

            return s + "}";
        }


        public static bool operator ==(SecRTuple left, SecRTuple right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.Labels.Count != right.Labels.Count)
                return false;

            for (int i = 0; i < left.Labels.Count; i++)
            {
                if (left.Labels[i] != right.Labels[i])
                    return false;
            }
            return true;
        }

        public static bool operator !=(SecRTuple left, SecRTuple right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is SecRTuple) && this == (SecRTuple)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public class SecRFun : SecRLabel
    {
        public List<SecRLabel> Args { get; private set; }
        public SecRLabel Ret { get; private set; }

        public SecRFun(List<SecRLabel> a, SecRLabel r)
        {
            Args = a;
            Ret = r;
        }

        public override string ToString()
        {
            string s = "fun(";

            for (int i = 0; i < Args.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Args[i].ToString();
            }

            return s + ") -> " + Ret.ToString();
        }

        public override Tuple<List<SecVar>, List<ISecPid>> Readers()
        {
            return Ret.Readers();
        }

        public static bool operator ==(SecRFun left, SecRFun right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (left.Args.Count != right.Args.Count)
                return false;

            for (int i = 0; i < left.Args.Count; i++)
            {
                if (left.Args[i] != right.Args[i])
                    return false;
            }
            return left.Ret == right.Ret;
        }

        public static bool operator !=(SecRFun left, SecRFun right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is SecRFun) && this == (SecRFun)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    public interface ISecPid
    {
    }

    public class SecPolicy
    {
        public ISecPid Owner { get; private set; }
        public List<ISecPid> Readers { get; private set; }

        public SecPolicy(ISecPid o, List<ISecPid> r)
        {
            Owner = o;
            Readers = r;
        }

        public override string ToString()
        {
            string s = "{ " + Owner.ToString() + " : ";
            for (int i = 0; i < Readers.Count; i++)
            {
                if (i > 0)
                    s += ", ";
                s += Readers[i].ToString();
            }
            return s + " }";
        }

        public static bool operator ==(SecPolicy left, SecPolicy right)
        {
            if (System.Object.ReferenceEquals(left, right))
                return true;

            if ((object)left == null || (object)right == null)
                return false;

            if (!ISecPid.Equals(left.Owner, right.Owner))
                return false;

            foreach (ISecPid sp in left.Readers)
            {
                bool found = false;
                foreach (ISecPid ssp in right.Readers)
                {
                    if (ISecPid.Equals(sp, ssp))
                    {
                        found = true;
                        break;
                    }
                }
                if (!found)
                    return false;
            }
            foreach (ISecPid sp in right.Readers)
            {
                bool found = false;
                foreach (ISecPid ssp in left.Readers)
                {
                    if (ISecPid.Equals(sp, ssp))
                    {
                        found = true;
                        break;
                    }
                }
                if (!found)
                    return false;
            }

            return true;
        }

        public static bool operator !=(SecPolicy left, SecPolicy right)
        {
            return !(left == right);
        }

        public override bool Equals(object obj)
        {
            return (obj is SecPolicy) && this == (SecPolicy)obj;
        }

        public override int GetHashCode()
        {
            return this.ToString().GetHashCode();
        }
    }

    [Serializable]
    public class SecLabelException : Exception
    {
        public SecLabelException() { }
        public SecLabelException(string message) : base(message) { }
        public SecLabelException(string message, Exception inner) : base(message, inner) { }
        protected SecLabelException(
          System.Runtime.Serialization.SerializationInfo info,
          System.Runtime.Serialization.StreamingContext context)
            : base(info, context) { }
    }
}
